PR summary 015b41b4dc

Import changes for modified files

No significant changes to the import graph

Declarations diff

No declarations were harmed in the making of this PR! 🐙

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

./scripts/technical-debt-metrics.sh pr_summary

Naïve question: Is proofwidgets the only dependency where this sort of thing needs to be checked? Could this happen with another new dependency that we add in the future?

Naïve question: Is proofwidgets the only dependency where this sort of thing needs to be checked? Could this happen with another new dependency that we add in the future?

So far it is only ProofWidgets, which does some shenanigans that I don't fully understand to retrieve precompiled artifacts so we don't need node installed to build Mathlib.

It's possible that Canonical will have similar difficulties if we ever manage to add that to Mathlib.

I just checked a recent commit of mathlib4 master and other than proofwidgets, it looks like LeanSearchClient is also on v4.25.0-rc1. I'm guessing it doesn't matter there and it'd be too strict for us to demand that all .lake/packages/*/lean-toolchain agree with lean-toolchain?

I just checked a recent commit of mathlib4 master and other than proofwidgets, it looks like LeanSearchClient is also on v4.25.0-rc1. I'm guessing it doesn't matter there and it'd be too strict for us to demand that all .lake/packages/*/lean-toolchain agree with lean-toolchain?

Yes, it would be a pain if the really minor libraries that don't depend on much Lean API needed to be bumped every release as well.

Thanks!
bors r+

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Post-Build Step